functor Palc (S : PALC_STRUCTS) : PALC =
struct
  open S
    structure A   = Ast    
    structure T   = Types
    structure E = ErrorMsg
    
    val error = E.error
    
     fun typeCktypenode(A.Int) = T.Intt
      |  typeCktypenode(A.Bool) = T.Boolt
      |  typeCktypenode(A.Void) = T.Voidt
      |  typeCktypenode(A.Struct(sid)) = T.Structt(sid,[])
      |  typeCktypenode(A.Pointer(btype)) = T.Pointt(typeCktypenode(btype))
      |  typeCktypenode(A.Array(size,btype)) = T.Arrayt(size,typeCktypenode(btype))
     
    fun typeCkidlist(tlist,vlist,[],p) = []
      | typeCkidlist(tlist,vlist,((newid,tp)::l),p) = 
        let  
           val tempt = typeCktypenode(tp) 
           val tempvarlist = (newid,tempt)::vlist
  	       fun isNotUsed [] = true
  	        |  isNotUsed ((var,tp)::l) = if(var=newid) then false else isNotUsed(l)  	       
        in if(T.isValidtp(tempt,tlist) andalso isNotUsed(vlist))
  	       then (newid,tempt)::typeCkidlist(tlist,tempvarlist,l,p)
  	       else (E.error p (": invalidate variable declaration! ");typeCkidlist(tlist,vlist,l,p))
        end
     
     fun typeCkstruct(tlist,sid,fields,p) = 
         let 
            val tmptypelist = T.Pointt(T.Structt(sid,[]))::tlist
   	        val flist = typeCkidlist(tmptypelist,[],fields,p)
   	        val returnt = [T.Structt(sid,flist)]
         in 
            if (T.isValidtp(T.Structt(sid,[]),tlist)) 
            then (E.error p (sid^": Duplicated Structure! ");([],[]))
   	        else (returnt,[])
         end      
    
      fun typeCkfuncdef(tlist,gvlist,arglist,fid,rtp,p) = 
          let 
              val tempt = typeCktypenode(rtp)
	          fun isNotUsed(fname,[]) = true
	           |  isNotUsed(fname,((gvname,gvtype)::l)) = if (gvname = fname) then false else isNotUsed(fname,(l))
	          val functype = T.Funct(arglist,tempt)
          in 
              if(fid = "main") 
              then (if((arglist = [])andalso(tempt = T.Voidt) andalso isNotUsed(fid,(gvlist)))
	                then [("main",functype)]
	                else (E.error p (fid^": Function definition error! ");[]))
	          else (if(T.isValidrettype(tempt,tlist)andalso isNotUsed(fid,gvlist))
	                then [(fid,functype)]
	                else (E.error p (fid^": Function definition error! ");[]))
          end   
  
     fun assertioncheck1 (tlist,gvlist,astnode)= 
      let 
          fun check(A.ExdecSkip) = ([],[])
	       |  check(A.ExdecSeq(node1,node2,p)) = 
	               let 
       	              val (t1,v1) = assertioncheck1(tlist,gvlist,node1)
       		          val ntlist = t1@tlist
       		          val nvlist = v1@gvlist
       		          val (t2,v2) = assertioncheck1(ntlist,nvlist,node2)
	               in 
	                  (t2@t1,v2@v1)
	               end
	       |  check(A.ExdecStruct(sid,fields,p)) = (typeCkstruct (tlist,sid,fields,p))
	       |  check(A.ExdecVar(idl,p)) = 
	               let 
	                   val neweles = List.rev(typeCkidlist(tlist,gvlist,idl,p))
	               in 
	                   ([],neweles)
	               end
	       |  check(A.ExdecFunc(fid,rtp,fargs,vdec,stm,prec,postc,p)) = 
	               let val tmplist = (fid,T.Errt)::gvlist
		               val arglist = typeCkidlist(tlist,tmplist,fargs,p)
		               val newgvlist = typeCkfuncdef(tlist,gvlist,arglist,fid,rtp,p)
	               in 
	                   ([],newgvlist)
	               end
      in 
          check astnode
      end
     
     
      fun typeCkbinop(bop,etp1,etp2) = 
        let fun  mapf (t1,t2) ocond t3 = 
	                if (T.eq(etp1,t1))andalso(T.eq(etp2,t2))orelse ocond
	                then t3
	                else T.Errt
	        fun   check A.Plus = mapf (T.Intt,T.Intt) false T.Intt
        	    | check A.Minus = mapf (T.Intt,T.Intt) false T.Intt
        	    | check A.Times = mapf (T.Intt,T.Intt) false T.Intt
        	    | check A.Divide = mapf (T.Intt,T.Intt) false T.Intt
        	    | check A.Modus = mapf (T.Intt,T.Intt) false T.Intt
        	    | check A.Band = mapf (T.Boolt,T.Boolt) false T.Boolt
        	    | check A.Bor = mapf (T.Boolt,T.Boolt) false T.Boolt
        	    | check A.Equ = mapf (T.Intt,T.Intt)
        				 (T.isPointertype(etp1) andalso T.isPointertype(etp2) andalso T.eq(etp1,etp2)) T.Boolt
        	    | check A.NEqu = mapf (T.Intt,T.Intt)
        				 (T.isPointertype(etp1) andalso T.isPointertype(etp2) andalso T.eq(etp1,etp2)) T.Boolt
        	    | check A.GT = mapf (T.Intt,T.Intt) false T.Boolt
        	    | check A.GE = mapf (T.Intt,T.Intt) false T.Boolt
        	    | check A.LT = mapf (T.Intt,T.Intt) false T.Boolt
        	    | check A.LE = mapf (T.Intt,T.Intt) false T.Boolt
        in check bop
        end
        
   
     fun typeCkexp(tlist,vlist,exp) =
        let 
           fun check (A.Expvoid) = T.Voidt
 	         | check (A.IntNum(i)) = T.Intt
	         | check (A.True) = T.Boolt
	         | check (A.False) = T.Boolt
	         | check (A.Null) = T.NS
	         | check (A.BinopExp(exp1,binop,exp2,p)) = 
	                  let 
	                      val t1 = check(exp1)
		                  val t2 = check(exp2)
		                  val etype = typeCkbinop(binop,t1,t2)
	                  in 
	                     if etype = T.Errt 
	                     then (E.error p (": binary operation error! ");etype)
		                 else etype
	                  end
	         | check (A.NotExp(exp,p)) = 
	                  let 
	                      val t = check(exp)
		                  fun isValid (t) = if t=T.Boolt then t else T.Errt
		                  val etype = isValid(t)
	                  in 
	                     if (etype = T.Errt) 
	                     then (E.error p (": unary operation error! "); etype)
		                 else etype
	                  end
	         | check (A.Lval(lval)) = typeCklval(tlist,vlist,lval)
	         | check (A.Imply(exp1,exp2,p)) = 
	                  let 
	                      val t1 = check(exp1)
		                  val t2 = check(exp2)
	                  in 
	                      if(t1=T.Boolt)andalso(t2=T.Boolt)
		                  then T.Boolt
		                  else(E.error p (": assertion type incorrect! ");T.Boolt)		     
	                  end
	         | check(A.Iff(exp1,exp2,p)) = 
	                 let 
	                     val t1 = check(exp1)
		                 val t2 = check(exp2)
	                 in 
	                    if(t1=T.Boolt)andalso(t2=T.Boolt)
		                then T.Boolt
		                else(E.error p (": assertion type incorrect! "); T.Boolt)	    
	                 end
	         | check(A.Forall(tid,atype,exp1,p)) = 
	                  let 
	                     val tempt = typeCktypenode(atype)
		                 val tvlist =(tid,tempt)::vlist
		                 val t1 = typeCkexp(tlist,tvlist,exp1)
	                  in 
	                     if(t1 = T.Boolt) 
		                 then T.Boolt
		                 else (E.error p (": assertion type incorrect! ");T.Boolt)		     
	                  end
	         | check(A.Exists(tid,atype,exp1,p)) = 
	                 let 
	                    val tempt = typeCktypenode(atype)
		                val tvlist =(tid,tempt)::vlist
		                val t1 = typeCkexp(tlist,tvlist,exp1)
   	                 in 
   	                    if(t1 = T.Boolt) 
   		                then T.Boolt
   		                else (E.error p (": assertion type incorrect! "); T.Boolt)		    
	                 end
	         | check(A.Pi(lvallists,p)) = 
	                 let 
	                     fun ckEach(tlval) = 
		                 let 
		                    val t = typeCklval(tlist,vlist,tlval)
		                 in 
		                    if(T.isPointertype(t))
			                then ()
			                else (E.error p (": pointer type required! "))
		                 end
		                 fun ckPinode[] = ()
		                   | ckPinode(node::l) = (ckEach(node);ckPinode(l))
		                 fun ckPiset [] = T.Boolt
		                   | ckPiset(node::l) = (ckPinode(node);ckPiset(l))
	                 in  
	                     ckPiset(lvallists)
	                 end
	         | check(A.N(lvallist,p)) = 
	                let  fun ckEach(tlval) = 
		                 let 
		                    val t = typeCklval(tlist,vlist,tlval)
		                 in 
		                    if(T.isPointertype(t))
			                then ()
			                else (E.error p (": pointer type required! "))
		                 end
		                 fun ckNset [] = T.Boolt
		                   | ckNset(node::l) = (ckEach(node);ckNset(l))
	                in   
	                     ckNset(lvallist)
	                end
	         | check(A.D(lvallist,p)) = 
	                let 
	                    fun ckEach(tlval) = 
		                let 
		                    val t = typeCklval(tlist,vlist,tlval)
		                 in 
		                    if(T.isPointertype(t))
			                then ()
			                else (E.error p (": pointer type required! "))
		                end
		                fun ckDset [] = T.Boolt
		                  | ckDset(node::l) = (ckEach(node);ckDset(l))
	                 in 
	                    ckDset(lvallist)
	                end
	         | check(A.Prev(lval,p)) = typeCklval(tlist,vlist,lval)
	         | check(A.Result) = 
	                let 
	                    fun findrettp[] = T.Errt
		                  | findrettp((name,tp)::l) = 
		                    if(name = "rettype")
		                    then tp
		                    else findrettp(l)
	                in 
	                    findrettp(vlist)
	                end
	        | check(A.LList(exp, pos)) =
	          let val ty = check exp
	          in  if T.isPointertype ty
	              then T.Boolt
	              else (error pos "pointer type expected"; T.Intt)
	          end
	        | check(A.Tree(exp, pos)) =
	          let val ty = check exp
	          in  if T.isPointertype ty
	              then T.Boolt
	              else (error pos "pointer type expected"; T.Intt)
	          end
	        | check _ = raise Fail "not impl\n"	        
        in check exp
        end
        
  and typeCklval(tlist,vlist,lval) =
        let 
          fun check (A.Var(vname,p)) = 
	      let 
	          fun gettype [] = T.Errt
		        | gettype ((name,tp)::l) = if vname = name then tp else gettype(l)		                  
		      val etype = gettype(vlist)
	      in 
	         if (etype = T.Errt) 
		     then (E.error p (vname^": undefined variable name! ");T.Errt)
		     else etype		    		 
	      end
	    | check (A.Inptr(blval,p)) = 
	      let val t = typeCklval(tlist,vlist,blval)
		      fun isPointer(T.Pointt(bt)) = bt
		        | isPointer(othertp) = T.Errt
		      val etype = isPointer(t)
	      in if etype = T.Errt 
		     then  (E.error p (": require a pointer type! ");T.Errt)
		      else etype		      		
	      end
	    | check (A.Inarray(blval,exp2,p)) = 
	      let val t1 = typeCklval(tlist,vlist,blval)
		      val t2 = typeCkexp(tlist,vlist,exp2)
		      fun isArray(T.Arrayt(size,bt)) = bt
		        | isArray(othertp) = T.Errt
		      val etype = isArray(t1)
	      in if (etype <> T.Errt)andalso(t2 = T.Intt) 
	         then etype
			 else (E.error p (": expression error (should be array)! ");etype)		     		      
	      end
	    | check (A.Instruct(slval,fname,p)) =
	      let val t = typeCklval(tlist,vlist,slval)
		      fun isStruct (T.Structt(name,dummy)) = T.getFieldtype(tlist,name,fname)
		        | isStruct(othertp) = T.Errt
		      val etype = isStruct(t)		 
	      in if etype= T.Errt 
	         then (E.error p (": cannot get the field type! "); T.Errt)
		     else etype		     		 
	      end
	    | check (A.Ptstruct(slval,fname,p)) = 
	      let val t = typeCklval(tlist,vlist,slval)
		      fun isStructPt (T.Pointt(T.Structt(name,dummy))) = T.getFieldtype(tlist,name,fname)		      
		        | isStructPt(othertp) = T.Errt
		      val etype = isStructPt(t)
	      in if etype= T.Errt 
	         then (E.error p (": cannot get the field type! ");T.Errt)
		     else etype		      		 
	      end
	    | check (A.Ptstruct2 (lval1, id1, id2, pos)) =
	      let val t = typeCklval(tlist, vlist, lval1)
	          val etype =
	              case t
	               of T.Pointt(T.Structt(name, dummy)) => T.getFieldtype(tlist, name, id1)		      
		        | _ => T.Errt
	      in case etype
	          of T.Errt => (E.error pos (": cannot get the field type! "); T.Errt)
		   | _ => etype
	      end
      in check lval
      end
      
     fun typeCkassert(tlist,vlist,ass) = 
          let 
              val t1 = typeCkexp(tlist,vlist,ass)
  	          val pos = case ass 
  	                  of A.BinopExp(e1,bo,e2,p) => p
  		               | A.Imply(e1,e2,p) => p
  		               | A.Iff(e1,e2,p) => p
  		               | A.Forall(id,tp,e,p) => p
  		               | A.Exists(id,tp,e,p) => p
  		               | A.Pi(list,p) => p
  		               | A.N(list,p) => p
  		               | A.D(list,p) => p
  		               | A.Prev(lval,p) => p
  		               | _ => 0
         in if(t1 = T.Boolt) then ()else (E.error pos (": the type of an assertion should be BOOL ! "))
         end
         
    fun typecheckinv (tlist,env,stms)=
        let 
           fun check(A.While(cond,inv,loopbody,p)) = typeCkassert(tlist,env,inv)
             | check _ =()
         
        in 
           check stms
        end
   
    fun bdfuncenv(tlist,gvlist,fid,vdec,p) = 
         let 
             fun findself [] = ([],T.Errt)
	           | findself((name,T.Funct(arglist,rettp))::l) = 
	                     if(name = fid) 
	                     then (arglist,rettp)
	                     else findself(l)
	           | findself(othernode::l) = findself(l)
	         val (alist,rettp) = findself(gvlist)
	         val tmp1list = List.rev(alist)@gvlist
	         val lvlist = typeCkidlist(tlist,tmp1list,vdec,p)
	         val tmp2list = List.rev(lvlist)@tmp1list
	         val _ = typeCkidlist(tlist,tmp2list,[("rettype",A.Int)],p)
         in 
            ("rettype",rettp)::tmp2list
         end  
     
      fun assertioncheck2(tlist,gvlist,astnode) = 
          let fun check(A.ExdecSkip) = ()
    	       |  check(A.ExdecSeq(node1,node2,p)) = (assertioncheck2(tlist,gvlist,node1);assertioncheck2(tlist,gvlist,node2))	      
    	       |  check(A.ExdecStruct(sid,fields,p)) = ()
    	       |  check(A.ExdecVar(idl,p)) = ()
    	       |  check(A.ExdecFunc(fid,rtp,fargs,vdec,stm,prec,postc,p)) = 
    	               let 
    		               val env = bdfuncenv(tlist,gvlist,fid,vdec,p)		            
    	               in 	                		             
    		              (typecheckinv(tlist,env,stm);
    		               typeCkassert(tlist,env,prec);
    		               typeCkassert(tlist,env,postc))		          		          
    	               end
          in 
              check astnode
          end     
       
    fun palc astnode=
      let 
            val typelist = T.Inittypelist()
            val libfunc = 
            ("printp",T.Funct([("p",T.Pointt(T.Voidt))],T.Voidt))::
			("print",T.Funct([("i",T.Intt)],T.Voidt))::
			("printb",T.Funct([("i",T.Boolt)],T.Voidt))::
			("alloc",T.Funct([("i",T.Intt)],T.Pointt(T.Voidt)))::
			("free",T.Funct([("ppp",T.Pointt(T.Voidt))],T.Voidt))::[]
		    val _ = print "assertion Type Checking ......\n"
	        val (t,v) = assertioncheck1(typelist,libfunc,astnode)	        
	   in        
	        assertioncheck2(t@typelist,v@libfunc,astnode)	  
      end

end
